(* A structure which contains the relevant identifiers and letctions of the Naive algorithm implementation, 
   adapted from the DICE 2010 paper. The algorithm pseudo-code can be found in "naive_algorithm.docx" *)
module NAIVE_ANALYSIS
open BJK
open FSEvent

(* composition operator for context-graphs *)
let (@@) (g1 : CG.graph) (g2 : CG.graph) = CG.compose(g1,g2)

(* LUB (join) operator for context-graphs *)

let (|||) (g1 : CG.graph) (g2 : CG.graph) = CG.join(g1,g2)

type DebugInfoAddedEventArgs(text : string) = 
    inherit System.EventArgs()
    member x.Text = text

let debugInfoAdded = new Event<DebugInfoAddedEventArgs>()
    
(* type AbstractInterpreter encapsulates the abstract interpreter algorithm, as described in abstractInterpreterAlgorithm.docx *)
type NaiveAnalysis(analysis_params : Analysis.ANALYSIS_PARMS) =
    let Debug = ref false
    
    [<CLIEvent>]
    member x.CommandGraphUpdated = commandGraphUpdated.Publish

    [<CLIEvent>]
    member x.DebugInfoAdded = debugInfoAdded.Publish
 
    (* the entry point for the abstact interpreter execution. Recieves a command of the core language as input (in AST form) and 
        returns a context-graph which represents the algorithm analysis results on the input command. *)
    member x.analyse(c : Core.Cmd) : CG.graph =  
            (* a global identifier which is updated (at the beginning of the algorithm execution) 
            to hold the number of variables in the analysed program. *)
        let numVars = ref 0;
        (* an iterator for debug print-out which is increased on each analysis interation over a loop body. *)
        let itCount = ref 0;
        (* debug mode -  when true - each algorithm stage will be printed, along with its output (and sometimes input). *)                
        (* Sends s to the any debug info added event listener. *)
        let debugPrint(s) = if (!Debug) then debugInfoAdded.Trigger(DebugInfoAddedEventArgs(s))

        let debugPrintG(g) = if (!Debug) then debugPrint(CG.prtEdges(g))
        (* returns flow i-(1)->i if i is not in source context and i <> x *)
        let computeFlowFromItoI(c : CoreEx.Cmd, i : int, x : int, srcContext : CG.Context) =
            if (i <> x && (not (CG.inContext(i,srcContext)))) then [(i,i,D.One,CoreEx.pat(c))] else [];

        (* computes context graph for commands of the form "X := 0" *)
        let computeAsgnZeroGraph(c : CoreEx.Cmd, x : int, preContexts : CG.Context list) : CG.graph =        
            let computeDataFlows(srcContext : CG.Context) : (mat.DataFlow) list =            
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->
                        computeFlowFromItoI(c,i,x,srcContext) @ computeMultipleFlows(i-1,srcContext);
            
                computeMultipleFlows((!numVars),srcContext)
                
                
            let computeEdge(srcContext : CG.Context) =             
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                (* include x in target context (equivalent to assignment of X := 0) *)
                let _ = CG.addVarToContext(x,tgtContext);
                let m = mat.M(computeDataFlows(srcContext));
                  
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(m, mat.r(m))) )
                
            
            CG.newGraph(List.map computeEdge preContexts)
              

        (* computes context graph for commands of the form "X := Y" *)
        let computeAsgnVarGraph(c : CoreEx.Cmd, x : int, y : int, preContexts : CG.Context list) : CG.graph =       
            let computeDataFlows(srcContext : CG.Context) : (mat.DataFlow) list =          
                let computeFlowFromYtoX(i : int, srcContext : CG.Context)  =
                    if (i = y && (not (CG.inContext(y, srcContext)))) then 
                        [(y,x,D.One,CoreEx.pat(c))]
                    else 
                        [];
              
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->                
                            let flowYtoX = computeFlowFromYtoX(i,srcContext);
                            let flowItoI = computeFlowFromItoI(c,i,x,srcContext);
                            flowYtoX @ flowItoI @ computeMultipleFlows(i-1, srcContext)
                       
                computeMultipleFlows((!numVars), srcContext)
               
                
            let computeEdge(srcContext : CG.Context) =            
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                let y_in_srcContext = CG.inContext(y, srcContext);
                (* add x to target context if y is in source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y, where Y <> 0) *)
                let () = CG.setVarInContext(x, tgtContext, y_in_srcContext); 
                let m = mat.M(computeDataFlows(srcContext));
            
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(m, [])) )
        
            CG.newGraph(List.map computeEdge preContexts)
               

        (* computes context graph for commands of the form "X := Y * Z" *)
        let computeAsgnTimesGraph(c : CoreEx.Cmd, x, y, z, preContexts) : CG.graph =         
            let computeDataFlows(srcContext : CG.Context) : (mat.DataFlow) list =            
                let computeSingleFlow(i : int, srcContext : CG.Context) : (mat.DataFlow) list =                
                    (* add flow y-(2)->x (or z-(2)->x) if y and z are both not in the source context (equivalent to assignment of X := Y*Z where Y>0 and Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : CG.Context) =
                        if ( (i = y || i = z) &&
                                (not (CG.inContext(y, srcContext) || CG.inContext(z, srcContext))) )
                        then [(i,x,analysis_params.nonlinear_Dvalue,CoreEx.pat(c))]
                        else [];
                
                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)
                
                let rec computeMultipleFlows = function 
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->
                        computeSingleFlow(i, srcContext) @ computeMultipleFlows(i-1, srcContext);
            
                computeMultipleFlows((!numVars), srcContext)
                
            let computeEdge(srcContext : CG.Context) =            
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                let y_or_z_in_srcContext = (CG.inContext(y, srcContext)) || (CG.inContext(z, srcContext));
                (* add x to target context if  y or z are in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y * Z, where Y>0 and Z > 0) *)
                let _ = CG.setVarInContext(x, tgtContext, y_or_z_in_srcContext); 
                let mat = mat.M(computeDataFlows(srcContext));
            
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(mat, [])) )
        
            CG.newGraph( List.map computeEdge preContexts )    

        (* computes context graph for commands of the form "X := Y + Z" *)    
        let computeAsgnPlusGraph(c : CoreEx.Cmd, x, y, z, preContexts) : CG.graph =        
            let computeDataFlows(x : int, y : int, z : int, srcContext : CG.Context) : (mat.DataFlow) list =            
                let computeSingleFlow(i : int, srcContext : CG.Context) : (mat.DataFlow) list =               
                    (* add flow y-(1')->x (or z-(1')->x) if y (or z) are not in the source context (equivalent to assignment of X := Y+Z where Y>0 or Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : CG.Context) =                   
                        let iNotInSrcContext = not (CG.inContext(i,srcContext))
                        let yInSrcContext = CG.inContext(y, srcContext)
                        let zInSrcContext = CG.inContext(z, srcContext)
                    
                        if (i = y || i = z) then
                            if (iNotInSrcContext && (not (yInSrcContext && zInSrcContext))) then 
                                if ((not yInSrcContext) && (not zInSrcContext)) then
                                    if y = z then
                                        [(i,x,D.Two,CoreEx.pat(c))] (* when the same var is added then we deduce polynomial growth *)
                                    else
                                        [(i,x,D.One',CoreEx.pat(c))]
                                else 
                                    [(i,x,D.One,CoreEx.pat(c))]
                            else []
                        else []
             
                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)
                
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->
                            computeSingleFlow(i,srcContext) @ computeMultipleFlows(i-1,srcContext);                                  
            
                computeMultipleFlows((!numVars),srcContext)
                
            let computeEdge(srcContext : CG.Context) =          
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                let y_and_z_in_srcContext = (CG.inContext(y, srcContext)) && (CG.inContext(z, srcContext));
                (* add x to target context if  y and z are both in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y + Z, where Y>0 or Z > 0) *)
                let _ = CG.setVarInContext(x, tgtContext, y_and_z_in_srcContext);  
                let m = mat.M(computeDataFlows(x,y,z,srcContext));
            
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(m, mat.r(m))) )        
        
            CG.newGraph( List.map computeEdge preContexts )


        (* updates DFRs on all edges of graph g with all possible data flows of the form (i->j,i'->j'). *)
        let computeDoubleFlows(g : CG.graph) =       
            let updateDoubleFlowsOnEdge = function
                | ( CG.E(p, q, refDfr) ) ->  
                    (* filter letction to determine if a given double data flow should be included in the result *)
                    let includeFlow (p : CG.Context,q : CG.Context) ((i,j),(i',j'),pat) = 
                                    (not (CG.inContext(i,p))) && (not (CG.inContext(i',p))) &&
                                    (not (CG.inContext(j,q))) && (not (CG.inContext(j',q))) &&
                                    (i <> i' || j <> j');
                    match !refDfr with
                    | (sop_bar.Dfr(m,_)) as dfr ->           
                            (* filter double flows according to source and target contexts *)
                            let r' = List.filter (includeFlow(p,q)) (mat.r(m));                        
                            refDfr := sop_bar.Dfr(m,r')
                | _ ->  Util.fail("NaiveAnalysis.updateDoubleFlowsOnEdge: Invalid argument.")     
     
     
            List.iter updateDoubleFlowsOnEdge (CG.edges(g))

        (* computes a graph corresponding to the abstract interpretation of an assignment command, with given pre-contexts *)
        let computeAssignmentGraph (c : CoreEx.Cmd, x : int, e : Core.Expr, preContexts : CG.Context list) : CG.graph =
            (* computes data flows of the form i-(d)->j *)
            let computeSingleFlows (x : int, e : Core.Expr, preContexts : CG.Context list) : CG.graph =
                match e with
                | Core.Zero ->                          computeAsgnZeroGraph(c, x, preContexts)
                | Core.Var y ->                          computeAsgnVarGraph(c,x, y, preContexts)
                | Core.Times(Core.Var y, Core.Var z) -> computeAsgnTimesGraph(c, x, y, z, preContexts)                                      
                | Core.Plus(Core.Var y , Core.Var z) -> computeAsgnPlusGraph(c, x, y, z, preContexts);
                | _ -> Util.fail("NaiveAnalysis.computeAssignmentGraph: Invalid argument.")
            
            let g' = ref (computeSingleFlows(x, e, preContexts));
            (* computes all data flows of the form (i->j,i'->j') over the flows calculated for all edges of the graph g' *)
            let () = computeDoubleFlows(!g');
            !g'
   
        (* a global ientifier which holds a list of all contexts - for ease of reference anywhere in the algorithm. *)
        let allContexts = ref ([CG.makeEmptyContext(1)]);

        (* the algorithm entry point - gets as input a command c and a list of pre-contexts and 
           returns the context-graph which corresponds to the command c. *)
        let rec naive(c : CoreEx.Cmd, preContexts : CG.Context list) : CG.graph =     
                (* Applies the loop correction operator on the context-graph g, according to loop rule L2 from the DICE paper. *)
                let rec doLoopCorrection(l : int, g : CG.graph) : CG.graph =
                        (* overload the * operator for DFRs for ease of expressiveness of the DFR composition (in this function only). *)
                        let (*) (d1 :sop_bar.DFR) (d2 :sop_bar.DFR) = sop_bar.prod(d1,d2);
                
                        (* applies the loop correction operator on a DFR *)
                        let rec LC(l,sop_bar.Dfr(m,r)) =                    
                            let m' = mat.LC (l, analysis_params.nonlinear_Dvalue, CoreEx.id(c)) m;                    
                            sop_bar.Dfr(m', sop_bar.filterR(r,m'))
                
                        (* computes LC on all edges (p,q') s.t. (p,q), (q,q') and (q,q) exist on graph. 
                           The result of this function is *)
                        let rec computeSingleEdge = function
                            | ( _, []) -> []
                            | ((CG.UE _), _) -> failwith "Unexpected appearance of UE"
                            | ((CG.E (p,q,d)) as e, (CG.E(p',q',d'))::t) ->
                                (if (CG.eqContexts(q,p')) then
                                    (match CG.getEdgeTag(g,CG.UE (q,q)) with
                                                    Some dfr -> [(CG.E (p,q', ref ( !d * LC(l, !dfr) * !d' ) ))] 
                                                           
                                                  | None     -> [])
                                 else []) @ computeSingleEdge(e,t)
                             | _ -> [];
                            
                        let rec computeMultipleEdges = function
                            | ([],_) -> []
                            | (e::t, fullEdgeList) ->
                                    computeSingleEdge(e,fullEdgeList) @ computeMultipleEdges(t,fullEdgeList);    
                
                        let sortedEdges = CG.sortEdges(CG.edges(g));
                
                        let () = CG.addEdges(g, computeMultipleEdges(sortedEdges, sortedEdges), false);
                        g
        
                (* computes a single iteration of a loop whose body is represented by the graph g (after some m >= 0 iterations). *)
                let rec doSingleIteration (g : CG.graph ref) g'  = 
                        let () = debugPrint("================================\nIteration #" + (!itCount).ToString() + ":\ncurrent graph(g):\n");
                        let () = debugPrintG(!g)
                        let () = debugPrint("graph to compose(g'):\n")
                        let () = debugPrintG(g')
                        let g'' = !g @@ g'
                        let () = debugPrint("composed graph(g''):\n")
                        let () = debugPrintG(g'')
                        let () = g := !g ||| g' ||| g''
                        let () = debugPrint("join result graph(g):\n")
                        let () = debugPrintG(!g)
                        let () = debugPrint("================================\n")
                        let () = itCount := !itCount + 1;
                        !g

                (* computes the result graph of any m > 0 iterations, where the input graph is the graph representing the loop-body and 
                   the possibility of 0 iterations (skip). This function corresponds to loop rule L1 from the DICE paper. *)        
                let rec doLoopClosure(x : int, g : CG.graph ref) : CG.graph =
                        let rec lfp f (g : CG.graph) =                   
                                let fg = (f g);                 
                                if (CG.equal(fg,g)) then g else lfp f fg
                
                        let g' = CG.newGraph(CG.edges(!g));
                        let () = itCount := 0;
                        lfp (doSingleIteration g) g'
            
        
                (* Computes the result graph of a loop whose body is represented by g and the iterating variable is x. *)
                let rec doLoop(x : int, g : CG.graph ref) : CG.graph =
                        (* the context graph g is joined with a graph which corresponds to the Skip command with the same pre-contexts.    
                           This action corresponds to applying loop rule L0 from the DICE paper. *)
                        let () = g := CG.join(!g, naive(CoreEx.NaiveCmd(CoreEx.Skip,-1), CG.preContexts(!g))) 
                        doLoopCorrection(x, doLoopClosure(x, g))
            
                let rec recurse(CoreEx.NaiveCmd(c,_) as c': CoreEx.Cmd, preContexts : CG.Context list) =
                    let g = match c with 
                            | CoreEx.Seq(c1,c2)      -> 
                                                            let g1 = naive(c1, preContexts);
                                                            let g2 = naive(c2, CG.postContexts(g1));    
                                                            g1 @@ g2
                                                
                            |  CoreEx.Choice(c1,c2)  -> naive(c1, preContexts) ||| naive(c2, preContexts)
                            |  CoreEx.Skip           -> computeAssignmentGraph(c', 1,Core.Var 1, !allContexts)
                            |  CoreEx.Asgn(i, e)     -> computeAssignmentGraph(c', i, e, !allContexts)
                            |  CoreEx.Loop(i, c')     -> doLoop(i, ref (naive(c', preContexts)));
                    commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c',g,""))
                    g
                    
                let () = debugPrint("starting to analyse command:\n");
                let () = debugPrint(CoreEx.prt(c));
                let () = debugPrint("Pre-contexts: " + CG.prtContexts(preContexts) + "\n");
                let g = recurse(c, preContexts);
                let () = debugPrint("Finished analysing command:\n");
                let () = debugPrint(CoreEx.prt(c));
                let () = debugPrint("graph:\n");
                let () = debugPrintG(g);
                let () = debugPrint("============================================\n");
                g

        let () = (numVars := Core.highest_var(c));
        let () = allContexts := CG.allContexts(!numVars)
        naive(CoreEx.extendedNaiveAST(c),[])
        
    member x.resultText(c, g : CG.graph) =
        let vars = Core.highest_var c 
        let bounded = ref [1..vars]
        let vt = BJKParse.parserLastVarToIndexMap()
        
        let rec prt_ints  = function
            | [] -> "\n"
            | i::rest -> let varFound = vt.ContainsKey(i)
                         (if varFound then vt.[i] else "") + (if varFound && rest<>[] then ", " + (prt_ints rest) else "\n")
       
        let removeNonBounded(b, nb) = 
            List.filter (fun x -> not (List.exists (fun y -> x=y) nb)) b
              
        for p in g.Keys do
            for et in g.[p].Values do  
                match !et with
                    | (sop_bar.Dfr(M,_)) ->
                            let (notbounded', _) = mat.classify(M,vars)
                            bounded := removeNonBounded(!bounded, notbounded')
        let nonbounded = List.filter (fun v -> not (List.exists (fun v' -> v'=v) !bounded)) [1..vars]            
        ("\n\nVARS: " + (vars.ToString()) + "\n" + analysis_params.name + ": " +
                 (prt_ints !bounded) + ("NON-" + analysis_params.name + ": ") + (prt_ints nonbounded)) 
    
    (* set the debug output mode *)
    member x.setDebugMode(mode : bool) = Debug := mode

let Poly = NaiveAnalysis(Analysis.PolyParams())        

let Lin = NaiveAnalysis(Analysis.LinParams())       